Step of Proof: p-first_wf 11,40
Inference at * 
Iof proof for Lemma p-first wf:


  A, B:Type, L:((A(B + Top)) List). p-first(L)  A(B + Top) 
latex
 by ((Unfold `p-first` 0) 
CollapseTHEN (Auto)) 
latex

Co.

Definitionsp-first(L), x.A(x), list_accum(x,a.f(x;a);y;l), x,y. t(x;y), inr x , , Unit, x:A. B(x), case b of inl(x) => s(x) | inr(y) => t(y), f(a), x:A.B(x), Void, type List, x:AB(x), left + right, Top, t  T, Type
Lemmaslist accum wf, it wf, top wf

origin